(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, 1).
The TRS R consists of the following rules:
primes → sieve(from(s(s(0))))
from(X) → cons(X, n__from(s(X)))
head(cons(X, Y)) → X
tail(cons(X, Y)) → activate(Y)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), n__filter(s(s(X)), activate(Z)), n__cons(Y, n__filter(X, sieve(Y))))
sieve(cons(X, Y)) → cons(X, n__filter(X, sieve(activate(Y))))
from(X) → n__from(X)
filter(X1, X2) → n__filter(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(X)
activate(n__filter(X1, X2)) → filter(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X
Rewrite Strategy: INNERMOST
(1) DependencyGraphProof (BOTH BOUNDS(ID, ID) transformation)
The following rules are not reachable from basic terms in the dependency graph and can be removed:
head(cons(X, Y)) → X
tail(cons(X, Y)) → activate(Y)
(2) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, 1).
The TRS R consists of the following rules:
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), n__filter(s(s(X)), activate(Z)), n__cons(Y, n__filter(X, sieve(Y))))
primes → sieve(from(s(s(0))))
if(true, X, Y) → activate(X)
activate(n__from(X)) → from(X)
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
from(X) → cons(X, n__from(s(X)))
filter(X1, X2) → n__filter(X1, X2)
if(false, X, Y) → activate(Y)
from(X) → n__from(X)
sieve(cons(X, Y)) → cons(X, n__filter(X, sieve(activate(Y))))
activate(n__filter(X1, X2)) → filter(X1, X2)
Rewrite Strategy: INNERMOST
(3) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)
The following defined symbols can occur below the 0th argument of cons: filter, sieve, cons, from, activate
The following defined symbols can occur below the 1th argument of cons: filter, sieve, cons, from, activate
The following defined symbols can occur below the 0th argument of activate: filter, sieve, cons, from, activate
The following defined symbols can occur below the 0th argument of sieve: filter, sieve, cons, from, activate
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), n__filter(s(s(X)), activate(Z)), n__cons(Y, n__filter(X, sieve(Y))))
(4) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, 1).
The TRS R consists of the following rules:
primes → sieve(from(s(s(0))))
from(X) → cons(X, n__from(s(X)))
filter(X1, X2) → n__filter(X1, X2)
if(false, X, Y) → activate(Y)
from(X) → n__from(X)
if(true, X, Y) → activate(X)
activate(n__from(X)) → from(X)
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
sieve(cons(X, Y)) → cons(X, n__filter(X, sieve(activate(Y))))
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__filter(X1, X2)) → filter(X1, X2)
Rewrite Strategy: INNERMOST
(5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
primes → sieve(from(s(s(0))))
from(z0) → cons(z0, n__from(s(z0)))
from(z0) → n__from(z0)
filter(z0, z1) → n__filter(z0, z1)
if(false, z0, z1) → activate(z1)
if(true, z0, z1) → activate(z0)
activate(n__from(z0)) → from(z0)
activate(z0) → z0
activate(n__cons(z0, z1)) → cons(z0, z1)
activate(n__filter(z0, z1)) → filter(z0, z1)
cons(z0, z1) → n__cons(z0, z1)
sieve(cons(z0, z1)) → cons(z0, n__filter(z0, sieve(activate(z1))))
Tuples:
PRIMES → c(SIEVE(from(s(s(0)))), FROM(s(s(0))))
FROM(z0) → c1(CONS(z0, n__from(s(z0))))
FROM(z0) → c2
FILTER(z0, z1) → c3
IF(false, z0, z1) → c4(ACTIVATE(z1))
IF(true, z0, z1) → c5(ACTIVATE(z0))
ACTIVATE(n__from(z0)) → c6(FROM(z0))
ACTIVATE(z0) → c7
ACTIVATE(n__cons(z0, z1)) → c8(CONS(z0, z1))
ACTIVATE(n__filter(z0, z1)) → c9(FILTER(z0, z1))
CONS(z0, z1) → c10
SIEVE(cons(z0, z1)) → c11(CONS(z0, n__filter(z0, sieve(activate(z1)))), SIEVE(activate(z1)), ACTIVATE(z1))
S tuples:
PRIMES → c(SIEVE(from(s(s(0)))), FROM(s(s(0))))
FROM(z0) → c1(CONS(z0, n__from(s(z0))))
FROM(z0) → c2
FILTER(z0, z1) → c3
IF(false, z0, z1) → c4(ACTIVATE(z1))
IF(true, z0, z1) → c5(ACTIVATE(z0))
ACTIVATE(n__from(z0)) → c6(FROM(z0))
ACTIVATE(z0) → c7
ACTIVATE(n__cons(z0, z1)) → c8(CONS(z0, z1))
ACTIVATE(n__filter(z0, z1)) → c9(FILTER(z0, z1))
CONS(z0, z1) → c10
SIEVE(cons(z0, z1)) → c11(CONS(z0, n__filter(z0, sieve(activate(z1)))), SIEVE(activate(z1)), ACTIVATE(z1))
K tuples:none
Defined Rule Symbols:
primes, from, filter, if, activate, cons, sieve
Defined Pair Symbols:
PRIMES, FROM, FILTER, IF, ACTIVATE, CONS, SIEVE
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11
(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 12 trailing nodes:
ACTIVATE(n__cons(z0, z1)) → c8(CONS(z0, z1))
FROM(z0) → c1(CONS(z0, n__from(s(z0))))
ACTIVATE(z0) → c7
SIEVE(cons(z0, z1)) → c11(CONS(z0, n__filter(z0, sieve(activate(z1)))), SIEVE(activate(z1)), ACTIVATE(z1))
IF(false, z0, z1) → c4(ACTIVATE(z1))
FILTER(z0, z1) → c3
ACTIVATE(n__filter(z0, z1)) → c9(FILTER(z0, z1))
CONS(z0, z1) → c10
PRIMES → c(SIEVE(from(s(s(0)))), FROM(s(s(0))))
FROM(z0) → c2
ACTIVATE(n__from(z0)) → c6(FROM(z0))
IF(true, z0, z1) → c5(ACTIVATE(z0))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
primes → sieve(from(s(s(0))))
from(z0) → cons(z0, n__from(s(z0)))
from(z0) → n__from(z0)
filter(z0, z1) → n__filter(z0, z1)
if(false, z0, z1) → activate(z1)
if(true, z0, z1) → activate(z0)
activate(n__from(z0)) → from(z0)
activate(z0) → z0
activate(n__cons(z0, z1)) → cons(z0, z1)
activate(n__filter(z0, z1)) → filter(z0, z1)
cons(z0, z1) → n__cons(z0, z1)
sieve(cons(z0, z1)) → cons(z0, n__filter(z0, sieve(activate(z1))))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
primes, from, filter, if, activate, cons, sieve
Defined Pair Symbols:none
Compound Symbols:none
(9) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(10) BOUNDS(1, 1)